$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$).
\\[0ex]ecl{-}trans{-}h($A$) $\in$ $\mathbb{N}\rightarrow$ecl{-}trans{-}type($A$)$\rightarrow\mathbb{B}$